21.3.4

题目

Is there a pair of types $(\mathrm{S},\mathrm{T})$ that is related by $\nu S$, but not by $\mu S$? What about a pair of types $(\mathrm{S},\mathrm{T})$ that is related by $\nu S_f$ , but not by $\mu S_f$ ?

解答

只写前半部分，这一部分书中给出的解答是错误的，errata 指出了这一点

只需证明形如 $(T,T)$，$T$ 为无穷类型的关系都在 $\nu S$ 中且不在 $\mu S$ 中

$\mathrm{\forall }T$，考虑集合 $R=\{(Q,Q\mid Q\text{ 是 T 的子树}\}$

容易验证，$R\subseteq S(R)$，根据 the principle of coinduction，$R\subseteq \nu S$，故 $(T,T)\subseteq R\subseteq \nu S$

现在，考虑集合 $M=\nu S-\{(T,T)\mid T\text{ 是无穷类型}\}$，下面验证 $S(M)\subseteq M$

由于 $S(M)\subseteq S(\nu S)=S$，只需证明 $S(M)\cap (\nu S-M)=\mathrm{\varnothing }$

而 $\nu S-M=\{(T,T)\mid T\text{ 是无穷类型}\}$，反证法：若存在无穷类型 $T$，$(T,T)\in S(M)$，则由 $S$ 的定义，以下三种情况必有至少一个满足：

Case 1:

但是这说明 $T=Top$，不可能

Case 2:

但是这说明 $S_1=T_1,S_2=T_2$，且 $S_1,S_2$ 中至少一个是无穷类型（否则 $S_1,S_2$ 均有穷，$T=S_1\times S_2$ 有穷，矛盾），不妨设为 $S_1$，那么 $(S_1,S_1)\in M$，与 $M$ 的定义矛盾

Case 3:

这也不可能，与 Case 2 同理

综上，以上三种情况均导出矛盾，$S(M)\subseteq M$ 得证

现在，根据 the principle of induction，$\mu S\subseteq M$，故对于任意无穷类型 $T$，$(T,T)\notin \mu S$

证毕